Nuprl Lemma : atom-free-Knd
0,22
postcript
pdf
k
:Knd. AtomFree(Knd;
k
)
latex
Definitions
left
+
right
,
Id
,
t
T
,
IdLnk
,
x
:
A
B
(
x
)
,
AtomFree(
T
;
x
)
,
x
:
A
.
B
(
x
)
,
Knd
,
<
a
,
b
>
,
inl(
x
)
,
x
.
A
(
x
)
,
inr(
x
)
Lemmas
atom-free-IdLnk
,
atom-free-Id
,
IdLnk
wf
,
Id
wf
origin
k:Knd. AtomFree(Knd;k) k:Knd. AtomFree(Knd;k) 
T
B(x)x:A. B(x)
x.A(x)